import Yices hiding (and, or, not, bits)
import qualified Yices as Y
import Data.List

-- A binary number is a sequence of bits.
type Binary = Nat -> Bool

-- Constants:
nn       = 5       -- size of board
n_s      = 24      -- how many stones at the beginning
n_e      = 2       -- how many stones at the end
width    = 5       -- how many bits in a Binary number
tt       = n_s-n_e -- how many steps to simulate
(hh, ww) = (nn, nn)

-- Variables in three flavors: v, v0, v1:
ss' :: Ident (Nat -> Nat -> Bool)
((ss',ss),(s0',s0),(s1',s1)) = decl ident2 "S"

t, h, v :: Term Binary
(t,t0,t1) = decl idnt "t"
(h,h0,h1) = decl idnt "h"
(v,v0,v1) = decl idnt "v"

d, b :: Term Bool
(d,d0,d1) = decl idnt "d"
(b,b0,b1) = decl idnt "b"

decl :: (String -> a) -> String -> (a, a, a)
decl i n = (i n, i (n ++ "0"), i (n ++ "1"))

idnt :: (Refl a) => String -> Term a
idnt = idt . ident

-- Binary representation of a number
infix 4 .=
(.=) :: Term Binary -> Nat -> Prop
b .= n = conj $ zipWith beq (take width $ bits n) [b ! nat i | i <- [1..]]
  where
    bits = unfoldr (Just . \x -> (odd x, x `div` 2))
    beq True  = id
    beq False = non

-- Successor arithmetic, tabular representation
follows :: Term Binary -> Term Binary -> Prop
x `follows` y = disj [ (x .= i+1) /\ (y .= i) | i <- [0..30]] 

-- All positions on the board, for convenience
board = [(i,j) | i <- [1..hh], j <- [1..ww]]

-- Initial and final state
initial, final :: Prop
-- We start at t = 0 with initial stone layout
initial = t .= 0 /\ conj [ if (i == 3 && j == 3) then non (ss i j) else ss i j | i <- [1..hh], j <- [1..ww]]
-- We end at t = tt, where we cannot make a move forward
final = t .= tt /\ deadEnd
  where
    deadEnd = non . disj . concat $
        [ [try i j   0   1  | i <- [1..hh], j <- [1..ww-2]]
        , [try i j   0 (-1) | i <- [1..hh], j <- [3..ww]]
        , [try i j   1   0  | i <- [1..hh-2], j <- [1..ww]]
        , [try i j (-1)  0  | i <- [3..hh], j <- [1..ww]]
        ]
    try i j p q = ss i j /\ ss (i+p) (j+q) /\ non (ss (i+p+p) (j+q+q))

-- Transition
trans :: Prop
trans = conj
    -- Time increases in each step
    [ conj [t1 `follows` t0]
    -- (v,h) points to a place on the board
    , disj [(v0 .= i) /\ (h0 .= j) | (i,j) <- board ]
    -- (v,h) pointing at a place requires a stone first to be there and then vanish
    , conj [(v0 .= i) /\ (h0 .= j) ==> s0 i j /\ non (s1 i j) | (i,j) <- board ]
    -- transformation of particular places at particular combinations of (d,b)
    , disj . map conj $ 
        [ [ d0     /\     b0 /\ disj [branch i j 0    1    | i <- [1..hh],   j <- [1..ww-2]]]
        , [ d0     /\ non b0 /\ disj [branch i j 0    (-1) | i <- [1..hh],   j <- [3..ww]]]
        , [ non d0 /\     b0 /\ disj [branch i j 1    0    | i <- [1..hh-2], j <- [1..ww]]]
        , [ non d0 /\ non b0 /\ disj [branch i j (-1) 0    | i <- [3..hh],   j <- [1..ww]]]
        ]
    ]
  where
    branch    i j p q = (v0 .= i) /\ (h0 .= j) /\ touched i j p q /\ untouched i j p q
    touched   i j p q = conj [s0 (i+p) (j+q), non $ s0 (i+p+p) (j+q+q), non $ s1 (i+p) (j+q), s1 (i+p+p) (j+q+q)]
    untouched i j p q = conj [s0 k l == s1 k l | (k,l) <- board, k /= i || l /= j, k /= i+p || l /= j+q, k /= i+p+p || l /= j+q+q]
    x == y     = iff' ! x ! y

main = printBddReach initial trans final
